Clock domain crossing (CDC) verification is useful in the verification process of integrated circuit (IC) design. CDC verification requires a combination of structural and functional analysis followed by a thorough review and debug of issues by the designer. A designer typically makes assumptions based on which constraints are provided to improve accuracy of the analysis and generate fewer violations in a next run. The functional analysis involves computation-intensive analysis which may lead to incomplete analysis (partial proof). A designer may need to decide on the validity of his design with partial results which may be error prone, making for a hard decision. CDC verification cannot be closed without functional verification. Assumptions may be made during CDC verification which are not validated at any point.
FIG. 1 is a flowchart 100 of a method of the prior art of formal CDC verification. In S110 a design of an IC and design constraints of the IC are received. In S120 structural verification is performed. In S130 the result is checked. If the result is a fail, execution continues with S140. Explicit assumptions are made in S140 to fix, assume or waive the design constraints and execution is reiterated to S110. The result of S130 may also be to pass under assumptions, in which case implicit assumptions are made. The result of S130 may also be to continue to functional verification, which is performed in S150. In S160 the result of the functional verification is checked. If the result is a fail, execution continues at S140. If the result is a pass or partial proof, execution ends. CDC verification may be closed with implicit assumptions, explicit assumptions and incomplete analysis.
In light of the deficiencies in the prior art, it would be advantageous to provide a system and method able to discover real design problems and provide clear guidance on when to close the verification process. It would be further advantageous that this process have a reasonable run time.